(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 (- v2 v0)))
(let ((e5 (- v1 v1)))
(let ((e6 (* v2 e3)))
(let ((e7 (distinct v0 v2)))
(let ((e8 (= v1 v1)))
(let ((e9 (>= v1 v0)))
(let ((e10 (= e4 e5)))
(let ((e11 (> e6 v2)))
(let ((e12 (ite e11 v0 v2)))
(let ((e13 (ite e7 e5 e12)))
(let ((e14 (ite e7 e6 e6)))
(let ((e15 (ite e8 v1 e5)))
(let ((e16 (ite e9 e12 e13)))
(let ((e17 (ite e7 e4 e15)))
(let ((e18 (ite e11 e6 v1)))
(let ((e19 (ite e10 e13 v2)))
(let ((e20 (<= e13 e17)))
(let ((e21 (distinct e13 v0)))
(let ((e22 (= e5 e5)))
(let ((e23 (<= e14 v1)))
(let ((e24 (>= e16 e14)))
(let ((e25 (= e12 e5)))
(let ((e26 (>= v2 e5)))
(let ((e27 (> v0 e17)))
(let ((e28 (distinct e5 e6)))
(let ((e29 (<= v1 e19)))
(let ((e30 (<= e5 e17)))
(let ((e31 (distinct v2 e6)))
(let ((e32 (>= e15 e6)))
(let ((e33 (= e13 v1)))
(let ((e34 (>= e4 e5)))
(let ((e35 (= e14 v2)))
(let ((e36 (<= e15 v1)))
(let ((e37 (< e6 e12)))
(let ((e38 (< v0 e13)))
(let ((e39 (< e12 v2)))
(let ((e40 (distinct e12 e18)))
(let ((e41 (or e38 e36)))
(let ((e42 (xor e27 e24)))
(let ((e43 (ite e39 e39 e23)))
(let ((e44 (and e26 e20)))
(let ((e45 (xor e8 e11)))
(let ((e46 (ite e28 e30 e28)))
(let ((e47 (or e34 e7)))
(let ((e48 (ite e31 e9 e45)))
(let ((e49 (xor e10 e25)))
(let ((e50 (xor e32 e44)))
(let ((e51 (= e29 e43)))
(let ((e52 (and e42 e46)))
(let ((e53 (= e22 e52)))
(let ((e54 (= e49 e49)))
(let ((e55 (xor e47 e21)))
(let ((e56 (not e35)))
(let ((e57 (not e50)))
(let ((e58 (= e53 e54)))
(let ((e59 (= e41 e55)))
(let ((e60 (and e48 e48)))
(let ((e61 (= e57 e56)))
(let ((e62 (and e60 e59)))
(let ((e63 (ite e40 e40 e61)))
(let ((e64 (ite e51 e51 e37)))
(let ((e65 (= e64 e64)))
(let ((e66 (=> e58 e63)))
(let ((e67 (= e65 e65)))
(let ((e68 (and e66 e62)))
(let ((e69 (or e68 e68)))
(let ((e70 (ite e67 e67 e69)))
(let ((e71 (not e33)))
(let ((e72 (xor e71 e70)))
e72
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

;; (assert (= v0 (/ (- 78) (- 77))))
;; (assert (= v1 (/ (- 5) 60)))
;; (assert (= v2 (/ 14 21)))
;; (check-sat)
(check-sat-assuming-model (v0 v1 v2) ((/ (- 78) (- 77)) (/ (- 5) 60) (/ 14 21)))
